This documents the changes from
leanprover/lean4#6744.

---------

Co-authored-by: David Thrane Christiansen <[email protected]>

)

this PR helps with bootstrapping leanprover#6744.

…prover#6744)

This PR extend the preprocessing of well-founded recursive definitions
to bring assumptions like `h✝ : x ∈ xs` into scope automatically.

This fixes leanprover#5471, and follows (roughly) the design written there.
See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean`
for details on the implementation.

This only works for higher-order functions that have a suitable setup.
See for example section “Well-founded recursion preprocessing setup” in
`src/Init/Data/List/Attach.lean`.

This does not change the `decreasing_tactic`, so in some cases there is
still the need for a manual termination proof some cases. We expect a
better termination tactic in the near future.

)

this PR helps with bootstrapping leanprover#6744.

…prover#6744)

This PR extend the preprocessing of well-founded recursive definitions
to bring assumptions like `h✝ : x ∈ xs` into scope automatically.

This fixes leanprover#5471, and follows (roughly) the design written there.
See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean`
for details on the implementation.

This only works for higher-order functions that have a suitable setup.
See for example section “Well-founded recursion preprocessing setup” in
`src/Init/Data/List/Attach.lean`.

This does not change the `decreasing_tactic`, so in some cases there is
still the need for a manual termination proof some cases. We expect a
better termination tactic in the near future.

)

this PR helps with bootstrapping leanprover#6744.

…prover#6744)

This PR extend the preprocessing of well-founded recursive definitions
to bring assumptions like `h✝ : x ∈ xs` into scope automatically.

This fixes leanprover#5471, and follows (roughly) the design written there.
See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean`
for details on the implementation.

This only works for higher-order functions that have a suitable setup.
See for example section “Well-founded recursion preprocessing setup” in
`src/Init/Data/List/Attach.lean`.

This does not change the `decreasing_tactic`, so in some cases there is
still the need for a manual termination proof some cases. We expect a
better termination tactic in the near future.

commit dcfd4a5f3f099bbed73dbc2a208d8474f1d7ea85
Author: Luisa Cicolini <[email protected]>
Date:   Tue Feb 18 14:50:39 2025 +0000

    chore: remove redundant

    Co-authored-by: Siddharth <[email protected]>

commit 9c1b8f6808ce667705de5ce57ea9f1b72b2b2b5a
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 23:31:09 2025 +0000

    chore: updated examples

commit c292ee8cd820bc92f87cba9929c237f8eec0b56d
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 23:13:52 2025 +0000

    chore: check simp onlys

commit d7d3abf838e0fa46a3082b372471bf28434b909f
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 23:11:37 2025 +0000

    chore: check simp onlys

commit b9b60410785709c42c8241738522e3916336d0f6
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 23:10:53 2025 +0000

    chore: check simp onlys

commit 4d509bf33bbc2ee315b9f4a022d571ffc2003c88
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 23:08:49 2025 +0000

    chore: fix umoo title format

commit c803b56fa6714bd23503a280f7e8d7ef74dc11d9
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 17:47:23 2025 +0000

    chore: fix build

commit 2d5b3519c4345c61b00dcfe0027bfefcd3438c59
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:43:11 2025 +0000

    chore: remove useless parentheses

    Co-authored-by: Tobias Grosser <[email protected]>

commit 8c6e69f8e88a7acf84e9cda565361ff7aad255c2
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:40:09 2025 +0000

    chore: remove useless parentheses

    Co-authored-by: Tobias Grosser <[email protected]>

commit bae2439078692dd5ba53be41e8db73a2ac275e29
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:39:55 2025 +0000

    chore: spacing format

    Co-authored-by: Tobias Grosser <[email protected]>

commit ed7af08600a3ebb9ac259f8733e151cb7bcca7e5
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:39:39 2025 +0000

    chore: remove useless parentheses

    Co-authored-by: Tobias Grosser <[email protected]>

commit 831cd70cfee4e656ff2d6c14c6d617025a395c03
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:34:15 2025 +0000

    chore: remove useless parentheses

    Co-authored-by: Tobias Grosser <[email protected]>

commit 1316186868f7508f815b858a625a11ee79b90fc7
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:34:01 2025 +0000

    chore: remove useless parentheses

    Co-authored-by: Tobias Grosser <[email protected]>

commit c5169062f6431d170e9ae5ce8f439994e6653177
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:33:04 2025 +0000

    chore: remove useless parentheses

    Co-authored-by: Tobias Grosser <[email protected]>

commit 7ec9ece80146e3d0c405f8adaf3e0c37cb02e66d
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 17:32:12 2025 +0000

    chore: golf toInt_intMax

    Co-authored-by: Siddharth <[email protected]>

commit a47b51f73a269c6bb30e4860071826db4c7d5af3
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 17:19:49 2025 +0000

    chore: golf toInt_intMax

commit 6ee013954e7269a1d509381e55a5314350dc13c5
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 17:14:55 2025 +0000

    chore: remove redundant coercion

commit 758bfad8aaaab377c89c6c7642f02ac745485119
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 16:05:41 2025 +0000

    chore: reuse previous proof

commit b7934d7c0f92defdcd4bf40bcb1f70990ad7f07d
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 15:49:54 2025 +0000

    chore: formatting

    Co-authored-by: Siddharth <[email protected]>

commit 66c3d7345db66eb726cc4e5b92c8f5f7b764523c
Author: Luisa Cicolini <[email protected]>
Date:   Mon Feb 17 15:49:43 2025 +0000

    chore: format

    Co-authored-by: Siddharth <[email protected]>

commit 0a8a754009c761e3f0dd1f3b5b7cc0a938f1f0f8
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 15:48:22 2025 +0000

    chore: less ugly proof

commit c1a32372d0ac4e78d46a26d5b868b0c664574951
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 15:43:04 2025 +0000

    chore: ugly proof

commit 42e0b5103d19318de9b8502038204b0e5b10f0c1
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 15:01:18 2025 +0000

    chore: fix toInt_intMax

commit e294f27d23646a656e7ae6b77cedf2c06424087c
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 10:36:00 2025 +0000

    chore: smul example

commit e00ebf97202321946b3839fd7aafc39dde0880e5
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:59:44 2025 +0000

    chore: replace theorem

commit 5379dad35e07d190f5ff739aaa6e1b2899a8946d
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:38:03 2025 +0000

    chore: format

commit a11b10b8d6abf66df36335fbb3f7b1868e8ac739
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:33:59 2025 +0000

    chore: fix example and format

commit 2de60122537568be3af0c376cc4aaccb08ecb264
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:29:09 2025 +0000

    chore: cleaning 3

commit 555157e7af39fafc1fdcbf30139c8f91d3a456b4
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:24:17 2025 +0000

    feat: add bv_decide test

commit 3aa2cdb17203dc837215667c3ebbc924763adaaa
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:14:44 2025 +0000

    chore: cleaning 2

commit be1e3ff03ccc82f12d0641a08ea92d356ca40cf8
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:11:31 2025 +0000

    chore: cleaning 1

commit 9bd164566de55d2399e4cc89f24b85136489270d
Author: luisacicolini <[email protected]>
Date:   Mon Feb 17 09:02:19 2025 +0000

    chore: fix sorrys

commit 38308335be8d8c29d04a3904b795caf6c71c0430
Author: Tobias Grosser <[email protected]>
Date:   Sun Feb 16 13:25:22 2025 +0000

    push sorry

commit 07cc6f48fc55c075cc86158aaad1611bcc411351
Merge: 07e89ce0bf f50b863868
Author: Tobias Grosser <[email protected]>
Date:   Sun Feb 16 13:17:40 2025 +0000

    Merge remote-tracking branch 'origin/master' into overflow-mul-defs

commit 07e89ce0bf58d74ea034365b1b0cb87701c04f3b
Author: Tobias Grosser <[email protected]>
Date:   Sun Feb 16 13:14:03 2025 +0000

    Fix the broken proofs

commit 6233f87e2f4230bea59e66c7404f34a79b204830
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 15 21:32:46 2025 -0800

    feat: cutsat helper functions (#7098)

    This PR adds some helper functions for cutsat in the `grind` tactic.

commit b94b704a6f169766277cbb9199157be45bab775a
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 15 18:52:14 2025 -0800

    feat: cutsat preparations (#7097)

    This PR implements several modifications for the cutsat procedure in
    `grind`.
    - The maximal variable is now at the beginning of linear polynomials.
    - The old `LinearArith.Solver` was deleted, and the normalizer was moved
    to `Simp`.
    - cutsat first files were created, and basic infrastructure for
    representing divisibility constraints was added.

commit fe6263754afc3d9872e078284d8b158d119d3366
Author: Tobias Grosser <[email protected]>
Date:   Sun Feb 16 00:04:56 2025 +0000

    feat: make `BitVec.getElem` the simp normal form and use it in `ext` (#5498)

    This PR makes `BitVec.getElem` the simp normal form in case a proof is
    available and changes `ext` to return `x[i]` + a hypothesis that proves
    that we are in-bounds. This aligns `BitVec` further with the API
    conventions of the Lean standard datatypes.

    We move our proofs to this new normal form, which results in slightly
    smaller proofs. With the exception of `getElem_ofFin`, no new API
    surface is added as the `getElem` API has already been completed over
    the previous months. We also move `getElem_shiftConcat_*` a bit higher
    as they are needed in earlier proofs. To keep the changeset small, we do
    not update the API of `BVDecide` but insert `←
    BitVec.getLsbD_eq_getElem` at the few locations where it is needed.
    Finally, we add a simproc for getElem, mirroring the existing ones for
    getLsbD/getMsdD.

    ---------

    Co-authored-by: Alex Keizer <[email protected]>

commit 29da643c15c5024161d73d6ddf2a0456a11585a1
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 15 15:45:35 2025 -0800

    chore: cleanup and missing `grind` normalization rules (#7095)

    This PR adds missing `grind` normalization rules, and removes dead
    theorems.

commit a9a1c8330a15f5039de2c1b4b1ba5e6ff32a92cd
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 15 14:10:23 2025 -0800

    refactor: add `denote'` functions to `Int/Linear.lean` (#7094)

    This PR adds the functions `Poly.denote'`, `RelCnstr.denote'`, and
    `DvdCnstr.denote'`. These functions are useful for representing the
    denotation of normalized results in `simp +arith` and the `grind`
    preprocessor. This PR also adjusts all auxiliary normalization theorems
    to use them to represent the normalized constraints. Previously, we were
    converting `RelCnstr` and `DvdCnstr` back into raw constraints. While
    this overhead was reasonable for `simp +arith`, it is not for the cutsat
    procedure, which has no need for raw constraints. All constraints have
    already been normalized by the time they reach cutsat.

commit b1c6a58b6ed5bc3df1eca38e040c49e512ea5e50
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 15 11:20:18 2025 -0800

    refactor: `Int.Linear` module (#7093)

    This PR cleans up the `Int.Linear` module by normalizing function and
    type names and adding documentation strings. We will use it to implement
    cutsat in the `grind` tactic.

commit f57029d0f39fe9023df2900a34b36d474d03bb76
Author: Leonardo de Moura <[email protected]>
Date:   Fri Feb 14 20:20:40 2025 -0800

    feat: divisibility constraint normalizer (#7092)

    This PR implements divisibility constraint normalization in `simp
    +arith`.

commit 12813e925986b020d0f2ac2e55be040917272d79
Author: jrr6 <[email protected]>
Date:   Fri Feb 14 22:00:36 2025 -0500

    fix: ensure `get_elem_tactic` works in absence of goals (#7088)

    This PR fixes the behavior of the indexed-access notation `xs[i]` in
    cases where the proof of `i`'s validity is filled in during unification.

    Closes #6999.

commit 81cf202725ad6a83adc6a1609fc8036c5cc7cf55
Author: Leonardo de Moura <[email protected]>
Date:   Fri Feb 14 18:44:49 2025 -0800

    feat: add helper theorems for normalizing divisibility constraints  (#7091)

    This PR adds helper theorems for normalizing divisibility constraints.
    They are going to be used to implement the cutsat procedure in the
    `grind` tactic.

commit c5f13132a24bf2bd736b29a47a0f84e03e67599c
Author: Kyle Miller <[email protected]>
Date:   Fri Feb 14 09:28:54 2025 -0800

    feat: make binders in `#check` be hoverable (#7074)

    This PR modifies the signature pretty printer to add hover information
    for parameters in binders. This makes the binders be consistent with the
    hovers in pi types.

    Suggested by @david-christiansen

commit c31d3e2cba169ae9ba419829fdfde35db275b712
Author: Markus Himmel <[email protected]>
Date:   Fri Feb 14 12:59:44 2025 +0100

    feat: `Fin.toNat` (#7079)

    This PR introduces `Fin.toNat` as an alias for `Fin.val`. We add this
    function for discoverability and consistency reasons. The normal form
    for proofs remains `Fin.val`, and there is a `simp` lemma rewriting
    `Fin.toNat` to `Fin.val`.

commit e98e635ff7c73005ca500efe830c40cac46b3336
Author: Markus Himmel <[email protected]>
Date:   Fri Feb 14 12:59:41 2025 +0100

    feat: `UIntX.ofNatTruncate` (#7080)

    This PR adds the functions `UIntX.ofNatTruncate` (the version for
    `UInt32` already exists).

commit dea6bf4c19a949addc2178464d470364cb4499bb
Author: Markus Himmel <[email protected]>
Date:   Fri Feb 14 12:59:37 2025 +0100

    feat: `IntX.minValue`, `IntX.maxValue`, `IntX.ofIntLE`, `IntX.ofIntTruncate` (#7081)

    This PR adds functions `IntX.ofIntLE`, `IntX.ofIntTruncate`, which are
    analogous to the unsigned counterparts `UIntX.ofNatLT` and
    `UInt.ofNatTruncate`.

commit 40b74248100d02392591fdb22acc55d859def24f
Author: Marc Huisinga <[email protected]>
Date:   Fri Feb 14 12:55:43 2025 +0100

    feat: request cancellation (#7054)

    This PR adds language server support for request cancellation to the
    following expensive requests: Code actions, auto-completion, document
    symbols, folding ranges and semantic highlighting. This means that when
    the client informs the language server that a request is stale (e.g.
    because it belongs to a previous state of the document), the language
    server will now prematurely cancel the computation of the response in
    order to reduce the CPU load for requests that will be discarded by the
    client anyways.

commit ade075bd22e854dc91f5fdb22cf1a1ea786dca29
Author: Marc Huisinga <[email protected]>
Date:   Fri Feb 14 12:53:24 2025 +0100

    fix: incremental goal state requests select incomplete snapshot (#6887)

    This PR fixes a bug where the goal state selection would sometimes
    select incomplete incremental snapshots on whitespace, leading to an
    incorrect "no goals" response. Fixes #6594, a regression that was
    originally introduced in 4.11.0 by #4727.

    The fundamental cause of #6594 was that the snapshot selection would
    always select the first snapshot with a range that contains the cursor
    position. For tactics, whitespace had to be included in this range.
    However, in the test case of #6594, this meant that the snapshot
    selection would also sometimes pick a snapshot before the cursor that
    still contains the cursor in its whitespace, but which also does not
    necessarily contain all the information needed to produce a correct goal
    state. Specifically, at the `InfoTree`-level, when the cursor is in
    whitespace, we distinguish competing goal states by their level of
    indentation. The snapshot selection did not have access to this
    information, so it necessarily had to do the wrong thing in some cases.

    This PR fixes the issue by adjusting the snapshot selection for goals to
    explicitly account for whitespace and indentation, and refactoring the
    language processor architecture to thread enough information through to
    the snapshot selection so that it can decide which snapshots to use
    without having to force too many tasks, which would destroy
    incrementality in goal state requests.

    Specifically, this PR makes the following adjustments:
    - Refactor `SnapshotTask` to contain both a `Syntax` and a `Range`.
    Before, `SnapshotTask`s had a single range that was used both for
    displaying file progress information and for selecting snapshots in
    server requests. For most snapshots, this range did not include
    whitespace, though for tactics it did. Now, the `reportingRange` field
    of `SnapshotTask` is intended exclusively for reporting file progress
    information, and the `Syntax` is used for selecting snapshots in server
    requests. Importantly, the `Syntax` contains the full range information
    of the snapshot, i.e. its regular range and its range including
    whitespace.
    - Adjust all call-sites of `SnapshotTask` to produce a reasonable
    `Syntax`.
    - Adjust the goal snapshot selection to account for whitespace and
    indentation, as the `InfoTree` goal selection does.
    - Fix a bug in the snapshot tree tracing that would cause it to render
    the `Info` of a snapshot at the wrong location when `trace.Elab.info`
    was also set.

    This PR is based on #6329.

commit 38a93e962052f7ee226a7e19b245600a5286f4f6
Author: Paul Reichert <[email protected]>
Date:   Fri Feb 14 09:24:33 2025 +0100

    feat: insertMany, ofList, ofArray, foldr, foldM functions for the tree map (#7051)

    This PR implements the methods `insertMany`, `ofList`, `ofArray`,
    `foldr` and `foldrM` on the tree map.

    ---------

    Co-authored-by: Paul Reichert <[email protected]>

commit 1c522cc2e2b5150a1cab09c82a114957a21d5b6b
Author: Markus Himmel <[email protected]>
Date:   Fri Feb 14 07:58:15 2025 +0100

    chore: rename `UIntX.ofNatCore`, `UIntX.ofNat'` -> `UIntX.ofNatLT` (#7071)

    This PR unifies the existing functions `UIntX.ofNatCore` and
    `UIntX.ofNat'` under a new name, `UIntX.ofNatLT`.

commit 523df207303806451d4037ed240050b72550bc0a
Author: Leonardo de Moura <[email protected]>
Date:   Thu Feb 13 21:43:38 2025 -0800

    feat: simprocs for `Int` and `Nat` divides predicates (#7078)

    This PR implements simprocs for `Int` and `Nat` divides predicates.

commit 7da2c917aada5957f7e05d8f3b9c2d97c6cb73b9
Author: Mac Malone <[email protected]>
Date:   Thu Feb 13 23:57:31 2025 -0500

    feat: lake: support plugins (#7001)

    This PR adds support for plugins to Lake. Precompiled modules are now
    loaded as plugins rather than via `--load-dynlib`.

    Additional plugins can be added through an experimental `plugins`
    configuration option. The syntax for specifying this is not yet
    convenient, and will be improved in future changes. A parallel `dynlibs`
    configuration option has been added for specifying additional dynamic
    libraries to build and pass to `--load-dynlib`.

    This PR also changes the default directory for `.olean`, `.ilean`, and
    module dynamic libraries (i.e., `leanLibDir`) to `lib/lean` instead of
    the previous default of `lib`. This avoids potential name clashes
    between single module shared libraries and the shared libraries of a
    full `lean_lib`.

    On non-Windows systems, module dynamic libraries are no longer linked to
    their imports or external symbols. Symbols from those libraries are left
    unresolved until load time. This avoids nesting these dependencies
    within the shared library and means Lake no longer needs to augment the
    shared library path to allow Lean to resolve such nested dependencies on
    load.

commit da4f887cbdb6caf6262a72ad9064d25f6446f803
Author: Leonardo de Moura <[email protected]>
Date:   Thu Feb 13 20:55:58 2025 -0800

    feat: support theorems for cutsat `Div-Solve` rule (#7077)

    This PR proves the helper theorems for justifying the "Div-Solve" rule
    in the cutsat procedure.

commit d01d43316154b0944da03eda828850f82bb5ee76
Author: Kim Morrison <[email protected]>
Date:   Fri Feb 14 15:08:18 2025 +1100

    feat: premise selection API (#7061)

    This PR provides a basic API for a premise selection tool, which can be
    provided in downstream libraries. It does not implement premise
    selection itself!

commit 383ffc121f0d2e914679cd9f45aea62a8bacc154
Author: Lean stage0 autoupdater <>
Date:   Thu Feb 13 16:00:29 2025 +0000

    chore: update stage0

commit cb856bcd8414a348c56da09bf8d41dafcdbb0dc4
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 15:51:42 2025 +0100

    chore: dsimproc for UIntX.ofNatLT (#7068)

    This PR is a follow-up to #7057 and adds a builtin dsimproc for
    `UIntX.ofNatLT` which it turns out we need in stage0 before we can get
    the deprecation of `UIntX.ofNatCore` in favor of `UIntX.ofNatLT` off the
    ground.

commit 37574d65b7e6efbe138c75f9579b5b46fd4f9843
Author: Bulhwi Cha <[email protected]>
Date:   Thu Feb 13 22:21:18 2025 +0900

    doc: fix typo (#7067)

commit e4d96ab4d38fc758b4b7bbb3b009d261ca5ecb51
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 13:52:31 2025 +0100

    chore: rename `BitVec.ofNatLt` -> `BitVec.ofNatLT` (#7064)

    This PR renames `BitVec.ofNatLt` to `BitVec.ofNatLT` and sets up
    deprecations for the old name.

commit a8053d1eb70b1adaa1907237609ae4f63cc0a2da
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 13:14:28 2025 +0100

    chore: rename `IntX.toNat` -> `IntX.toNatClampNeg` (#7066)

    This PR renames `IntX.toNat` to `IntX.toNatClampNeg` (to reduce
    surprises) and sets up a deprecation.

commit 7a887d60ae3f8a35eaaf488acccf1e6858d233be
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 12:29:31 2025 +0100

    chore: make `IntX` constructor private, provide `UIntX.toIntX` (#7062)

    This PR introduces the functions `UIntX.toIntX` as the public API to
    obtain the `IntX` that is 2's complement equivalent to a given `UIntX`.

commit 6b46cf583c0ed4f489305264a22a4d55e10f9f3a
Author: Paul Reichert <[email protected]>
Date:   Thu Feb 13 12:12:22 2025 +0100

    feat: deprecated find, fold, foldM, mergeBy functions for the tree map (#7036)

    This PR adds some deprecated function aliases to the tree map in order
    to ease the transition from the `RBMap` to the tree map.

    ---------

    Co-authored-by: Paul Reichert <[email protected]>

commit 37827565d23ce62c3898dcd532c6a3021e262cef
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 12:02:00 2025 +0100

    feat: missing conversion functions for `ISize` (#7063)

    This PR adds `ISize.toInt8`, `ISize.toInt16`, `Int8.toISize`,
    `Int16.toISize`.

commit 2ebedea21a49e0f060ffcc045caaf1781636726e
Author: Joachim Breitner <[email protected]>
Date:   Thu Feb 13 10:38:42 2025 +0100

    feat: binderNameHint in congr (#7053)

    This PR makes `simp` heed the `binderNameHint` also in the assumptions
    of congruence rules. Fixes #7052.

commit ab65a54dec15f293b21f3e62e4e0ad822ae99a8f
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 09:45:01 2025 +0100

    feat: `UIntX.ofFin` (#7056)

    This PR adds the `UIntX.ofFin` conversion functions.

commit 0c219197ff2596d9525546ab752893870dc7e78b
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 13 08:50:47 2025 +0100

    chore: rename `UIntX.val` -> `UIntX.toFin` (#7050)

    This PR renames the functions `UIntX.val` to `UIntX.toFin`.

commit a5fdbb12896f82bbfb0500372d0943efa1209a31
Author: Kim Morrison <[email protected]>
Date:   Thu Feb 13 14:19:02 2025 +1100

    chore: upstream an Int lemma (#7060)

commit 6a586e67d9b8448d8c43b81d1e61756a8969a759
Author: Leonardo de Moura <[email protected]>
Date:   Wed Feb 12 15:16:07 2025 -0800

    refactor: move `grind` offset constraint module to `Grind/Arith/Offset` (#7058)

    This PR moves the `grind` offset constraint module to the
    `Grind/Arith/Offset` subdirectory in preparation to the full linear
    integer arithmetic module.

commit ec514da34fc2a93b90f4515c2c213c04fdfe2b33
Author: Lean stage0 autoupdater <>
Date:   Wed Feb 12 17:09:23 2025 +0000

    chore: update stage0

commit 76f5c3746024a2b7bb9be32a34d10341d6f7101a
Author: Markus Himmel <[email protected]>
Date:   Wed Feb 12 17:08:03 2025 +0100

    chore: rename `UIntX.mk` -> `UIntX.ofBitVec` (#7046)

    This PR renames `UIntX.mk` to `UIntX.ofBitVec` and adds deprecations.

commit 40630e6ea9b0dec005e46d0cf08a3656fef0d0c1
Author: Markus Himmel <[email protected]>
Date:   Wed Feb 12 16:12:29 2025 +0100

    chore: add `UIntX.ofNatLT` (#7057)

    This PR adds the function `UIntX.ofNatLT`. This is supposed to be a
    replacement for `UIntX.ofNatCore` and `UIntX.ofNat'`, but for
    bootstrapping reasons we need this function to exist in stage0 before we
    can proceed with the renaming and deprecations, so this PR just adds the
    function.

commit 3fd31da818c2b86fe523aaac313b26897e0f1938
Author: Markus Himmel <[email protected]>
Date:   Wed Feb 12 15:49:31 2025 +0100

    feat: `IntX.ofBitVec` (#7048)

    This PR adds the functions `IntX.ofBitVec`.

commit daddcb81147fbf423e64ae9de6f4cba6dffa02c5
Author: Joachim Breitner <[email protected]>
Date:   Wed Feb 12 14:22:08 2025 +0100

    feat: propagate wfParam through let (#7039)

    This PR improves the well-founded definition preprocessing to propagate
    `wfParam` through let expressions.

    Fixes #7038.

commit 995751bdd506422ab66e5297d2f08c4ab8976b85
Author: Sebastian Ullrich <[email protected]>
Date:   Wed Feb 12 10:29:51 2025 +0100

    chore: compile against glibc 2.26 (#7037)

    This PR relaxes the minimum required glibc version for Lean and Lean
    executables to 2.26 on x86-64 Linux

commit ea02231b46e122b9b099684e2ffee637884f200f
Author: Sebastian Ullrich <[email protected]>
Date:   Wed Feb 12 10:19:30 2025 +0100

    chore: remove `save` tactic (#7047)

    This PR removes the `save` and `checkpoint` tactics that have been
    superseded by incremental elaboration

commit 3a91e7a0499d0a316c78ba620c75276e4f0cf8c9
Author: Cameron Zwarich <[email protected]>
Date:   Wed Feb 12 01:13:49 2025 -0800

    fix: make several LCNF environment extensions have asyncMode of .sync (#7041)

    This PR marks several LCNF-specific environment extensions as having an
    asyncMode of .sync rather than the default of .mainOnly, so they work
    correctly even in async contexts.

commit 5b5fbcd86ed2b42fd5093b357ca6a2333e20c02d
Author: Joachim Breitner <[email protected]>
Date:   Wed Feb 12 10:06:12 2025 +0100

    feat: wf_preprocess for {List,Array}.Monadic functions (#7034)

    This PR adds `wf_preprocess` theorems for
    `{List,Array}.{foldlM,foldrM,mapM,filterMapM,flatMapM}`

commit d4ccc335279e53683f80b1b1ceffa93593452698
Author: Sebastian Ullrich <[email protected]>
Date:   Wed Feb 12 11:22:32 2025 +0100

    test: fix `simp_arith1` benchmark (#7049)

commit ca764bd88abd9ffef64c6729f509d23eeb3fc8dd
Author: Lean stage0 autoupdater <>
Date:   Wed Feb 12 09:15:43 2025 +0000

    chore: update stage0

commit 9dbbc4823dcd3a3dd356445b6167b70f59adf91d
Author: Kim Morrison <[email protected]>
Date:   Wed Feb 12 16:17:39 2025 +1100

    chore: fix `linter.listVariables` naming (#7044)

commit 64fb473fa735f98385c3c1d3604a4237190fb139
Author: Leonardo de Moura <[email protected]>
Date:   Tue Feb 11 19:55:45 2025 -0800

    chore: `simp_arith` has been deprecated (#7043)

    This PR deprecates the tactics `simp_arith`, `simp_arith!`,
    `simp_all_arith` and `simp_all_arith!`. Users can just use the `+arith`
    option.

commit e4b50ac5ae692d1e3641b748f2058cf5bbe4bf39
Author: Leonardo de Moura <[email protected]>
Date:   Tue Feb 11 18:14:00 2025 -0800

    chore: remove dead code from `Nat/Linear.lean` (#7042)

commit a37d386aca0b634f8b6ac4e376157afb50895e65
Author: Leonardo de Moura <[email protected]>
Date:   Tue Feb 11 15:37:30 2025 -0800

    feat: `simp +arith` sorts linear atoms (#7040)

    This PR ensures that terms such as `f (2*x + y)` and `f (y + x + x)`
    have the same normal form when using `simp +arith`

commit 73e20798bd147b5d15685797a33c22d510d3a475
Author: Paul Reichert <[email protected]>
Date:   Tue Feb 11 15:47:47 2025 +0100

    feat: tree map data structures and operations (#6914)

    This PR introduces ordered map data structures, namely `DTreeMap`,
    `TreeMap`, `TreeSet` and their `.Raw` variants, into the standard
    library. There are still some operations missing that the hash map has.
    As of now, the operations are unverified, but the corresponding lemmas
    will follow in subsequent PRs. While the tree map has already been
    optimized, more micro-optimization will follow as soon as the new code
    generator is ready.

    ---------

    Co-authored-by: Paul Reichert <[email protected]>

commit bbd41d5374ba1603c41ecc94ff85002f62691167
Author: Henrik Böving <[email protected]>
Date:   Tue Feb 11 12:01:40 2025 +0100

    feat: present bv_decide counter examples for UIntX and enums better (#7033)

    This PR improves presentation of counter examples for UIntX and enum
    inductives in bv_decide.

commit f07e640ddb08499a3256fe55d51712243f9656da
Author: Leonardo de Moura <[email protected]>
Date:   Mon Feb 10 19:45:25 2025 -0800

    feat: linear integer inequality normalization using `gcd` of coefficients (#7030)

    This PR adds completes the linear integer inequality normalizer for
    `grind`. The missing normalization step replaces a linear inequality of
    the form `a_1*x_1 + ... + a_n*x_n + b <= 0` with `a_1/k * x_1 + ... +
    a_n/k * x_n + ceil(b/k) <= 0` where `k = gcd(a_1, ..., a_n)`.
    `ceil(b/k)` is implemented using the helper `cdiv b k`.

commit 8abeb42c4f744919578f60be94edf5d230d88986
Author: Mac Malone <[email protected]>
Date:   Mon Feb 10 19:43:38 2025 -0500

    feat: lake: provide help on Elan's `+` option (#7024)

    This PR documents how to use Elan's `+` option with `lake new|init`. It
    also provides an more informative error message if a `+` option leaks
    into Lake (e.g., if a user provides the option to a Lake run without
    Elan).

commit 0e328f06781d9881a8838b13bf03a03805804cc2
Author: Sebastian Ullrich <[email protected]>
Date:   Mon Feb 10 19:16:20 2025 +0100

    chore: build Lean with `Elab.async` (#6989)

commit 519f70cc1c7b72e51089a5d52d5164826510b91d
Author: Henrik Böving <[email protected]>
Date:   Mon Feb 10 18:42:59 2025 +0100

    feat: bv_decide rewrite multiplication with power of two to shift (#7029)

    This PR adds simprocs to bv_decide's preprocessor that rewrite
    multiplication with powers of two to constant shifts.

commit 45e5deb1acfb717caf720cc5359297ffc6c62a97
Author: Sebastian Ullrich <[email protected]>
Date:   Mon Feb 10 17:44:05 2025 +0100

    chore: trivial changes from async-proofs branch (#7028)

commit 98e0e308c72ce0168de01bf5838fc44b0f4d6bcb
Author: Joachim Breitner <[email protected]>
Date:   Mon Feb 10 17:43:41 2025 +0100

    feat: nested well-founded recursion via automatic preprocessing (#6744)

    This PR extend the preprocessing of well-founded recursive definitions
    to bring assumptions like `h✝ : x ∈ xs` into scope automatically.

    This fixes #5471, and follows (roughly) the design written there.
    See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean`
    for details on the implementation.

    This only works for higher-order functions that have a suitable setup.
    See for example section “Well-founded recursion preprocessing setup” in
    `src/Init/Data/List/Attach.lean`.

    This does not change the `decreasing_tactic`, so in some cases there is
    still the need for a manual termination proof some cases. We expect a
    better termination tactic in the near future.

commit bb5a71d6d32d970a6323b9ff30e486fc5015429e
Author: Lean stage0 autoupdater <>
Date:   Mon Feb 10 16:30:51 2025 +0000

    chore: update stage0

commit dfc1eeb8c2ae15ab8453ad8a6315a0a4048cab7c
Author: Markus Himmel <[email protected]>
Date:   Mon Feb 10 16:27:30 2025 +0100

    doc: misc. style guide and naming scheme additions (#7026)

    This PR clarifies the styling of `do` blocks, and enhanes the naming
    conventions with information about the `ext` and `mono` name components
    as well as advice about primed names and naming of simp sets.

commit ca73817b5c83ac3e7877c77f6acbef3b926c30b5
Author: Sebastian Ullrich <[email protected]>
Date:   Mon Feb 10 16:08:02 2025 +0100

    fix: codegen was allowed improper env ext accesses (#7023)

commit f5d861f4294b6b17713a152572377fdc9049185b
Author: Kim Morrison <[email protected]>
Date:   Tue Feb 11 01:20:18 2025 +1100

    chore: rename simp sets (#7017)

    This PR renames the simp set `boolToPropSimps` to `bool_to_prop` and
    `bv_toNat` to `bitvec_to_nat`. I'll be adding more similarly named simp
    sets.

commit 6584cb93b237d98fd46ac0fe35ca5fe0a5c37ee4
Author: Kim Morrison <[email protected]>
Date:   Tue Feb 11 00:49:17 2025 +1100

    chore: deprecated compile_time_search_path% (#7022)

    This PR deprecates `compile_time_search_path%`; it didn't prove useful,
    and we've shot ourselves in the foot with it more than once.

commit b70fb04ba69b1ea14b330bd476ae7a39343b88eb
Author: Henrik Böving <[email protected]>
Date:   Mon Feb 10 14:48:20 2025 +0100

    feat: add basic extract theorems for bv_decide (#7021)

    This PR adds theorems for interactions of extractLsb with `&&&`, `^^^`,
    `~~~` and `bif` to bv_decide's preprocessor.

commit 17ef9f8c6e01491ff92dc9042d54f27177bbc134
Author: Kim Morrison <[email protected]>
Date:   Mon Feb 10 23:17:44 2025 +1100

    feat: improvements to simp confluence (#7013)

    This PR makes improvements to the simp set for List/Array/Vector/Option
    to improve confluence, in preparation for `simp_lc`.

commit 497946851699b3c128e9ae4fdbbe835f8e5caf33
Author: Henrik Böving <[email protected]>
Date:   Mon Feb 10 12:24:52 2025 +0100

    fix: correct trace nodes in bv_decide (#7019)

    This PR properly spells out the trace nodes in bv_decide so they are
    visible with just `trace.Meta.Tactic.bv` and `trace.Meta.Tactic.sat`
    instead of always having to enable the profiler.

commit f2762ac06d3dbbc7d8e3ed62f92f6874c13e62be
Author: Lean stage0 autoupdater <>
Date:   Mon Feb 10 11:58:06 2025 +0000

    chore: update stage0

commit ec8eb9a6e9ee5df67521bd181b189f7ebf06088d
Author: Sebastian Ullrich <[email protected]>
Date:   Mon Feb 10 11:56:49 2025 +0100

    chore: `Task.get` block profiling (#7016)

    * `--profile` now reports `blocking` time spent in `Task.get` inside
    other profiling categories
    * environment variable `LEAN_TRACE_TASK_GET_BLOCKED` when set makes
    `lean` dump stack traces of `Task.get` blocks

commit 057c72f545c325564734b50ebd3c03f881fe4bc5
Author: Kim Morrison <[email protected]>
Date:   Mon Feb 10 21:56:20 2025 +1100

    chore: rename simp sets (#7018)

    This is preliminary to #7017; we'll need an update-stage0 before the
    actual rename can take place.

commit 93b622f05869605a47a2a9cefd170f558631a95f
Author: Kim Morrison <[email protected]>
Date:   Mon Feb 10 21:37:21 2025 +1100

    chore: replace HashMap.get_ lemmas with getElem_ versions (#7004)

    This PR replaces various `HashMap.get_X` with `getElem_X` versions. Now
    the left hand sides are in simp normal form (and this fixes some
    confluence problems).

commit 8b65ab0be4c66508fb93cc0ef32f619d4d097a80
Author: Kim Morrison <[email protected]>
Date:   Mon Feb 10 21:30:41 2025 +1100

    chore: add @[simp] to List.flatten_toArray (#7014)

commit db2b9e4663b4a74791e2b724bc6a6a72776ee3db
Author: Henrik Böving <[email protected]>
Date:   Mon Feb 10 11:00:20 2025 +0100

    feat: basic support for handling enum inductives in bv_decide (#6946)

    This PR implements basic support for handling of enum inductives in
    `bv_decide`. It now supports equality on enum inductive variables (or
    other uninterpreted atoms) and constants.

commit c51d82c8408c056f5e4e9a752906529bd36b71df
Author: Leonardo de Moura <[email protected]>
Date:   Sun Feb 9 22:13:28 2025 -0800

    feat: `simp +arith` normalizes coefficient in linear integer polynomials (#7015)

    This PR makes sure `simp +arith` normalizes coefficients in linear
    integer polynomials. There is still one todo: tightening the bound of
    inequalities.

commit 59c602fd808c1b00eaf8bfb6d2739de254f3c5dd
Author: Kim Morrison <[email protected]>
Date:   Mon Feb 10 09:54:51 2025 +1100

    chore: unprotect List.foldlM (#7003)

commit 290e5311f971f2410d734b9694b8ad3fcc8e8c00
Author: Leonardo de Moura <[email protected]>
Date:   Sun Feb 9 14:46:09 2025 -0800

    chore: improve `withAbstractAtoms` (#7012)

    We should not abstract free variables

commit 9769781a083bbb760155863e77ccd9ddd803a143
Author: Leonardo de Moura <[email protected]>
Date:   Sun Feb 9 13:41:58 2025 -0800

    feat: `simp +arith` for integers (#7011)

    This PR adds `simp +arith` for integers. It uses the new `grind`
    normalizer for linear integer arithmetic. We still need to implement
    support for dividing the coefficients by their GCD. It also fixes
    several bugs in the normalizer.

commit dc8073e54f8deee3223fc388490f9ca50c869be9
Author: Leonardo de Moura <[email protected]>
Date:   Sun Feb 9 09:24:07 2025 -0800

    chore: improve `expose_names` doc string (#7010)

commit 5b5b52ab88918ad1766787c60319554978e4557c
Author: Leonardo de Moura <[email protected]>
Date:   Sun Feb 9 09:11:28 2025 -0800

    feat: `bv_decide` hint (#7009)

    This PR ensures users get an error message saying which module to import
    when they try to use `bv_decide`.

commit 12b2f731180ccf80c3ed290491dae489ce29bc59
Author: Kim Morrison <[email protected]>
Date:   Mon Feb 10 03:20:38 2025 +1100

    chore: remove unused Int simp lemmas (#7005)

commit 940afe624efaf6ffb428fdacee8a4c5f77c01696
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 8 20:32:54 2025 -0800

    feat: linear integer arith normalizer (#7002)

    This PR implements the normalizer for linear integer arithmetic
    expressions. It is not connect to `simp +arith` yet because of some
    spurious `[simp]` attributes.

commit 00d884c49802fcd338c252c7b70b31c2bd491b68
Author: Leonardo de Moura <[email protected]>
Date:   Sat Feb 8 15:01:01 2025 -0800

    feat: add `Int.Linear` normalization support (#7000)

    This PR adds helper theorems for justifying the linear integer
    normalizer.

commit 859015f335d2b13acbe50a29deda909c1ea8575b
Author: Kyle Miller <[email protected]>
Date:   Sat Feb 8 10:11:26 2025 -0800

    doc: mention `Prop`s are equal to `True` or `False` (#6998)

    This PR modifies the `Prop` docstring to point out that every
    proposition is propositionally equal to either `True` or `False`. This
    will help point users toward seeing that `Prop` is like `Bool`.

    I considered mentioning `Classical.propComplete`, but it's probably
    better not making it seem like that's how you should work with
    propositions.

commit 869a2b9cbda726f0b2289d8821d4f18ce2fadbfe
Author: Bolton Bailey <[email protected]>
Date:   Sat Feb 8 07:04:39 2025 -0800

    chore: change Lake configuration error message (#6829)

    This PR changes the error message for Lake configuration failure to
    reflect that issues do not always arise from an invalid lakefile, but
    sometimes arise from other issues like network errors. The new error
    message encompasses all of these possibilities.

    Closes #6827

commit 2392d4abe443cfd495da2026bbfa044395ddd19e
Author: Joachim Breitner <[email protected]>
Date:   Sat Feb 8 11:32:34 2025 +0100

    refactor: elaborate forIn notation without extra let (#6977)

    This PR avoids a `let` in the elaboration of `forIn`. It was introduced
    in https://github.com/leanprover/lean4/commit/f51328ff112 but nothing
    seems to break when I simplify the code. This removes an unexpected `let
    col✝ :=…` from the “Expected type” view in the Info View and from the
    termination proofs.

commit dea9fcec136c60cba0a58cf4e157ce77e2f6d359
Author: Leonardo de Moura <[email protected]>
Date:   Fri Feb 7 14:43:30 2025 -0800

    feat: `exact?` in `try?` (#6995)

    This PR implements support for `exact?` in the `try?` tactic.

commit a6f14f52e5d4ee7063ee6f318da8df9d506f2ada
Author: Leonardo de Moura <[email protected]>
Date:   Fri Feb 7 11:17:25 2025 -0800

    feat: compress `try?` suggestions (#6994)

    This PR adds the `Try.Config.merge` flag (`true` by default) to the
    `try?` tactic. When set to `true`, `try?` compresses suggestions such
    as:
    ```lean
    · induction xs, ys using bla.induct
        · grind only [List.length_reverse]
        · grind only [bla]
    ```
    into:
    ```lean
    induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla]
    ```

    This PR also ensures `try?` does not generate suggestions that mixes
    `grind` and `grind only`, or `simp` and `simp only` tactics.

    This PR also adds the `try? +harder` option (previously called `lib`),
    but it has not been fully implemented yet.

commit 20f5666ce2b2d041ebed7d3f805c4ab849619a01
Author: Leonardo de Moura <[email protected]>
Date:   Fri Feb 7 11:13:50 2025 -0800

    chore: disable broken test

    It is timing out on OSX, and `master` is failing to build.
    This is a temporary "fix."

commit 8ab3a81901b79fcd65c84ccc7923d5ab6cb0d3b4
Author: Sebastian Ullrich <[email protected]>
Date:   Fri Feb 7 17:50:31 2025 +0100

    feat: parallel progress notifications (#6329)

    This PR enables the language server to present multiple disjoint line
    ranges as being worked on. Even before parallelism lands, we make use of
    this feature to show post-elaboration tasks such as kernel checking on
    the first line of a declaration to distinguish them from the final
    tactic step.

    ![image](https://github.com/user-attachments/assets/f6170689-6835-40c0-baba-df067a60b605)

commit f3d8c6be9d64c13874740a27b334afba18ce6dab
Author: Leonardo de Moura <[email protected]>
Date:   Fri Feb 7 08:33:25 2025 -0800

    feat: improve `try?` suggestion (#6991)

    This PR improves how suggestions for the `<;>` combinator are generated.

commit 8c297201e0f806d49fdac48554e911b8a2732c69
Author: Sebastian Ullrich <[email protected]>
Date:   Fri Feb 7 17:12:31 2025 +0100

    chore: re-enable `Elab.async` in the server (#6990)

commit 14c4620cd2f83be2f50ec41f597c0d7532b27b73
Author: Sebastian Ullrich <[email protected]>
Date:   Fri Feb 7 16:55:32 2025 +0100

    fix: convert kernel interrupt into elab interrupt (#6988)

    This PR ensures interrupting the kernel does not lead to wrong, sticky
    error messages in the editor

commit 64794357be33dc4695ffad7896383711e65e0e7a
Author: Sebastian Ullrich <[email protected]>
Date:   Fri Feb 7 16:33:10 2025 +0100

    feat: API to avoid deadlocks from dropped promises (#6958)

    This PR improves the `Promise` API by considering how dropped promises
    can lead to never-finished tasks.

commit 73d7a3f6ae93c667e184f6888348e5828d8e0880
Author: Sebastian Ullrich <[email protected]>
Date:   Fri Feb 7 11:14:35 2025 +0100

    perf: avoid taking mutex on already-resolved promises (#6984)

commit 3824513a51e5205849a867da39eb71ee6e9e45cb
Author: Sebastian Ullrich <[email protected]>
Date:   Fri Feb 7 10:06:57 2025 +0100

    feat: respect `Task.map/bind (sync := true)` after waiting (#6976)

    This PR extends the behavior of the `sync` flag for `Task.map/bind` etc.
    to encompass synchronous execution even when they first have to wait on
    completion of the first task, drastically lowering the overhead of such
    tasks. Thus the flag is now equivalent to e.g. .NET's
    `TaskContinuationOptions.ExecuteSynchronously`.

commit 17a5c420b1723f1ba0156480d6b966feb589a9d4
Author: Kim Morrison <[email protected]>
Date:   Fri Feb 7 15:02:02 2025 +1100

    feat: improve monadic Array lemmas (#6982)

    This PR improves some lemmas about monads and monadic operations on
    Array/Vector, using @Rob23oa's work in
    https://github.com/leanprover-community/batteries/pull/1109, and
    adding/generalizing some additional lemmas.

commit dccbb94b0b98cc3df1513498308e0fabd56231f4
Author: Kim Morrison <[email protected]>
Date:   Fri Feb 7 12:44:51 2025 +1100

    chore: linting List (#6970)

commit a246933999b5ecc988a1d0035df2a7b78b191039
Author: Leonardo de Moura <[email protected]>
Date:   Thu Feb 6 17:35:41 2025 -0800

    feat: `try?` tactic improvements (#6981)

    This PR adds new configuration options to `try?`.
    - `try? -only` omits `simp only` and `grind only` suggestions
    - `try? +missing` enables partial solutions where some subgoals are
    "solved" using `sorry`, and must be manually proved by the user.
    - `try? (max:=<num>)` sets the maximum number of suggestions produced
    (default is 8).

commit 5355badf854ec3dbddd793d97a3c25f43bb1b0c7
Author: Leonardo de Moura <[email protected]>
Date:   Thu Feb 6 15:59:38 2025 -0800

    feat: `try?` validation and cleanup (#6980)

    This PR improves the `try?` tactic runtime validation and error
    messages. It also simplifies the implementation, and removes unnecessary
    code.

commit 89f643b8e7a2403d42d2e751f00788c94bf49d7c
Author: Sofia Rodrigues <[email protected]>
Date:   Thu Feb 6 20:24:42 2025 -0300

    feat: improve some files separation and standardize error messages in UV modules (#6830)

    This PR improves some files separation and standardize error messages in
    UV modules

commit 4ac6d0807a437476b45b47ff0e8311a466284283
Author: Leonardo de Moura <[email protected]>
Date:   Thu Feb 6 13:56:14 2025 -0800

    feat: `try?` composite suggestions (#6979)

    This PR adds support for more complex suggestions in `try?`. Example:
    ```lean
    example (as : List α) (a : α) : concat as a = as ++ [a] := by
      try?
    ```
    suggestion
    ```
    Try this: · induction as, a using concat.induct
      · rfl
      · simp_all
    ```

commit 1d42ab8be66135a7a7511ead28ed64bc5b9bc9e8
Author: Marc Huisinga <[email protected]>
Date:   Thu Feb 6 20:26:11 2025 +0100

    fix: inlay hints in untitled files (#6978)

    This PR fixes a bug where both the inlay hint change invalidation logic
    and the inlay hint edit delay logic were broken in untitled files.
    Thanks to @Julian for spotting this!

commit da5d7760ae5cd62541b5721efee67ffa15f887c6
Author: Lean stage0 autoupdater <>
Date:   Thu Feb 6 17:39:42 2025 +0000

    chore: update stage0

commit 65c0674ba2c2d7b0b2296466946f185479cedcf5
Author: Marc Huisinga <[email protected]>
Date:   Thu Feb 6 17:43:56 2025 +0100

    feat: inlay hint refinements (#6959)

    This PR implements a number of refinements for the auto-implicit inlay
    hints implemented in #6768.
    Specifically:
    - In #6768, there was a bug where the inlay hint edit delay could
    accumulate on successive edits, which meant that it could sometimes take
    much longer for inlay hints to show up. This PR implements the basic
    infrastructure for request cancellation and implements request
    cancellation for semantic tokens and inlay hints to resolve the issue.
    With this edit delay bug fixed, it made more sense to increase the edit
    delay slightly from 2000ms to 3000ms.
    - In #6768, we applied the edit delay to every single inlay hint request
    in order to reduce the amount of inlay hint flickering. This meant that
    the edit delay also had a significant effect on how far inlay hints
    would lag behind the file progress bar. This PR adjusts the edit delay
    logic so that it only affects requests sent directly after a
    corresponding `didChange` notification. Once the edit delay is used up,
    all further semantic token requests are responded to without delay, so
    that the only latency that affects how far the inlay hints lag behind
    the progress bar is how often we emit refresh requests and how long VS
    Code takes to respond to them.
    - For inlay hints, refresh requests are now emitted 500ms after a
    response to an inlay hint request, not 2000ms, which means that after
    the edit delay, inlay hints should only lag behind the progress bar by
    about up to 500ms. This is justifiable for inlay hints because the
    response should be much smaller than e.g. is the case for semantic
    tokens.
    - In #6768, 'Restart File' did not prompt a refresh, but it does now.
    - VS Code does not immediately remove old inlay hints from the document
    when they are applied. In #6768, this meant that inlay hints would
    linger around for a bit once applied. To mitigate this issue, this PR
    adjusts the inlay hint edit delay logic to identify edits sent from the
    client as being inlay hint applications, and sets the edit delay to 0ms
    for the inlay hint requests following it. This means that inlay hints
    are now applied immediately.
    - In #6768, hovering over single-letter auto-implicit inlay hints was a
    bit finicky because VS Code uses the regular cursor icon on inlay hints,
    not the thin text cursor icon, which means that it is easy to put the
    cursor in the wrong spot. We now add the separation character (` ` or
    `{`) preceding an auto-implicit to the hover range as well, which makes
    hovering over inlay hints much smoother.

commit acb971a81a5f0f509253dfeaced92df7de0e1ed9
Author: Lean stage0 autoupdater <>
Date:   Thu Feb 6 12:27:11 2025 +0000

    chore: update stage0

commit db885bb7fb8196ef56d8014b44c65db5321016e0
Author: Joachim Breitner <[email protected]>
Date:   Thu Feb 6 12:28:23 2025 +0100

    refactor: rename auto_attach attribute to wf_preprocess (#6972)

    As per dicussion with team colleages, the feature shouldn’t be called
    “auto attach” but rather “well-founded recursion preprocessing” to avoid
    (imprecise) jargon.

commit ad7371de69868b161a1b3befa46715f694db1785
Author: Henrik Böving <[email protected]>
Date:   Thu Feb 6 12:16:57 2025 +0100

    refactor: bv_decide's type analysis to prepare for enum support (#6971)

    This PR does some refactoring on bv_decide's type analysis in
    preparation for enum support in #6946.

commit 32a22d81e9ef675f411792d560ba9419466f90dc
Author: Joachim Breitner <[email protected]>
Date:   Thu Feb 6 12:03:27 2025 +0100

    feat: binderNameHint (#6947)

    This PR adds the `binderNameHint` gadget. It can be used in rewrite and
    simp rules to preserve a user-provided name where possible.

    The expression `binderNameHint v binder e` defined to be `e`.

    If it is used on the right-hand side of an equation that is applied by a
    tactic like `rw` or `simp`,
    and `v` is a local variable, and `binder` is an expression that (after
    beta-reduction) is a binder
    (so `fun w => …` or `∀ w, …`), then it will rename `v` to the name used
    in the binder, and remove
    the `binderNameHint`.

    A typical use of this gadget would be as follows; the gadget ensures
    that after rewriting, the local
    variable is still `name`, and not `x`:
    ```
    theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
        l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry

    example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
      rw [all_eq_not_any_not]
      -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
    ```

    This gadget is supported by `simp`, `dsimp` and `rw` in the
    right-hand-side of an equation, but not
    in hypotheses or by other tactics.

commit 9e9b29f5f3f23e7514d934a68211388a2505023f
Author: Kim Morrison <[email protected]>
Date:   Thu Feb 6 21:20:17 2025 +1100

    chore: rename Nat.not_eq_zero_of_lt (#6968)

    Renames a lemma.

    Closes #6714

commit c5bc29568fd6cf14f58bf2725d2a34513fcd0bd1
Author: Markus Himmel <[email protected]>
Date:   Thu Feb 6 09:33:48 2025 +0100

    doc: style guide and naming convention for the standard library (#6950)

    This PR adds a style guide and a naming convention for the standard
    library.

commit 1f905640257a28f33b118930af0cd52d633eab15
Author: Lean stage0 autoupdater <>
Date:   Thu Feb 6 08:27:23 2025 +0000

    chore: update stage0

commit 9bcb48157fadc661ae51677128688112fb4d1490
Author: Leonardo de Moura <[email protected]>
Date:   Wed Feb 5 21:44:25 2025 -0800

    feat: use `expose_names` in `try?` (#6967)

    This PR ensures `try?` can suggest tactics that need to reference
    inaccessible local names.
    Example:
    ```lean
    /--
    info: Try these:
    • · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
    • · expose_names; induction as, bs_1 using app.induct <;> grind only [app]
    -/
    #guard_msgs (info) in
    example : app (app as bs) cs = app as (app bs cs) := by
      have bs := 20 -- shadows `bs` in the target
      try?
    ```

commit f458b99779c0e5e45c31a312426d016f271ceea1
Author: Kim Morrison <[email protected]>
Date:   Thu Feb 6 15:49:21 2025 +1100

    feat: add internal linter for List/Array/Vector variable names (#6966)

    This PR adds an internal-use-only strict linter for the variable names
    of `List`/`Array`/`Vector` variables, and begins cleaning up.

commit fa5ac2ec5bfea3d2bd8bfedf6a7c3a2cb97562c9
Author: Leonardo de Moura <[email protected]>
Date:   Wed Feb 5 20:47:26 2025 -0800

    feat: implement `try?` using `evalAndSuggest` (#6965)

    This PR re-implements the `try?` tactic using the new `evalAndSuggest`
    infrastructure.

commit b62b9d4ce6e1a630ae9d365c18f2fae99e024673
Author: Kim Morrison <[email protected]>
Date:   Thu Feb 6 14:11:53 2025 +1100

    feat: `#info_trees in` command (#6964)

    This PR adds a convenience command `#info_trees in`, which prints the
    info trees generated by the following command. It is useful for
    debugging or learning about `InfoTree`.

commit 00dc96ef6163f26ef281b73d5463b9138b0e9e4a
Author: Kim Morrison <[email protected]>
Date:   Thu Feb 6 13:39:06 2025 +1100

    chore: further cleanup of index variable naming in List (#6963)

commit 6c0d0ef74ab86167d731b828b1c5878c4ff7576c
Author: Kim Morrison <[email protected]>
Date:   Thu Feb 6 12:56:47 2025 +1100

    doc: improve List.toArray doc-string (#6962)

    This PR improves the doc-string for `List.toArray`.

    Thanks to @jt0202 for pointing this out.

commit 8ade4a54e533202224023ce2ea179a44458ba348
Author: Leonardo de Moura <[email protected]>
Date:   Wed Feb 5 14:13:47 2025 -0800

    feat: `evalAndSuggest` helper tactic (#6961)

    This PR adds the auxiliary tactic `evalAndSuggest`. It will be used to
    refactor `try?`.

commit f0b956830df0732fa45036a7c03fae33854ffa6c
Author: Lean stage0 autoupdater <>
Date:   Wed Feb 5 16:42:25 2025 +0000

    chore: update stage0

commit dc9806e9d569432651f17114463ba582ea39f213
Author: jrr6 <[email protected]>
Date:   Wed Feb 5 10:43:54 2025 -0500

    feat: allow updating binders to and from strict- and instance-implicit (#6634)

    This PR adds support for changing the binder annotations of existing
    variables to and from strict-implicit and instance-implicit using the
    `variable` command.

    This PR requires a stage0 update to fully take effect.

    Closes #6078

commit c7ee39543fb63fe22bf9e1a6f47f4780e650ef54
Author: Lean stage0 autoupdater <>
Date:   Wed Feb 5 14:42:28 2025 +0000

    chore: update stage0

commit 973a745bc0209410868d88b00521343725fab4e3
Author: Joachim Breitner <[email protected]>
Date:   Wed Feb 5 14:33:35 2025 +0100

    feat: add `auto_attach` simp set (no functionality yet) (#6956)

    this PR helps with bootstrapping #6744.

commit f65dc78c4f6aca25f142ede951ac5f76866c8eb3
Author: Tobias Grosser <[email protected]>
Date:   Sun Feb 16 11:45:30 2025 +0000

    Update src/Init/Data/BitVec/Lemmas.lean

commit d7d39848d91720c5bf1a9ec957cb017c087e229b
Author: Tobias Grosser <[email protected]>
Date:   Sun Feb 16 11:44:51 2025 +0000

    Update src/Init/Data/BitVec/Lemmas.lean

commit 94a68d45584ffd70b6154012732564df083adfaa
Author: luisacicolini <[email protected]>
Date:   Tue Feb 11 08:41:18 2025 +0000

    chore: smul correct def

commit 87b1a873ae804c96995dc201debdb655749616f2
Author: luisacicolini <[email protected]>
Date:   Mon Feb 10 10:36:13 2025 +0000

    chore: simplify mul_le_mul_self

commit 24e9bc92578c91ae9cb66754d27381671139757a
Author: luisacicolini <[email protected]>
Date:   Mon Feb 10 09:31:36 2025 +0000

    chore: fix theorem name

commit 67d5900e5445ef8de1e608771ed4d0860d90d652
Author: luisacicolini <[email protected]>
Date:   Mon Feb 10 09:30:51 2025 +0000

    chore: fix theorem name

commit 155971c6072ff8fd1f8cd87160446ea784cfa0c9
Author: Siddharth Bhat <[email protected]>
Date:   Thu Feb 6 14:36:55 2025 +0000

    chore: shorter proof of toInt_one_of_lt

commit 89a87da466e1890dcb88d73b9293ab197677f04c
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 14:08:28 2025 +0000

    chore: undo unwanted change

commit fcce13fc5da7e39ac4cbf82d34809f72686d2f09
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 13:56:26 2025 +0000

    chore: more cleaning

commit 1ebc9b43a406f4291bc42ecf5dfa7aedbc076419
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 11:45:02 2025 +0000

    chore: undo unwanted change

commit 199f7cc993bb7c3c64b8fe7de2436c442b28ccf0
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 11:44:51 2025 +0000

    chore: undo unwanted change

commit cc7128ffeee09b84a68dd990308da79dcd482a81
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 11:44:36 2025 +0000

    chore: undo unwanted change

commit 7509cb60d4929db13ffcd0dd824291c8709b6936
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 11:44:04 2025 +0000

    chore: undo unwanted change

commit a9527249b93d6a246f789fbcd21667a239a67151
Author: luisacicolini <[email protected]>
Date:   Thu Feb 6 11:43:23 2025 +0000

    chore: bring the theorems back home

commit 6f7469b430f88b9425c05f3554030101d062cf2c
Author: luisacicolini <[email protected]>
Date:   Wed Feb 5 18:52:05 2025 +0000

    chore: clean proof

commit dee6fa2f91daa36a7eda1b1290f8a9fa0665aa92
Author: Tobias Grosser <[email protected]>
Date:   Wed Feb 5 16:52:06 2025 +0000

    drop sorries

commit 741107e68ed8e325b14f806b6b88384380395dab
Author: luisacicolini <[email protected]>
Date:   Wed Feb 5 14:36:48 2025 +0000

    chore: giving up

commit 43b174e0be48259b36202daf14e572a8a346955d
Author: luisacicolini <[email protected]>
Date:   Wed Feb 5 12:42:46 2025 +0000

    chore: fix build

commit 5786b41d55f8a0f3ab19b8aa53fbed20a127f127
Author: luisacicolini <[email protected]>
Date:   Wed Feb 5 11:38:34 2025 +0000

    chore: reorder theorems

commit f7d800aada32f68fd97948e731afc37fb904ce63
Merge: 540349d567 53ed233f38
Author: Luisa Cicolini <[email protected]>
Date:   Wed Feb 5 11:37:59 2025 +0000

    Merge branch 'master' into overflow-mul-defs

commit 540349d567e58395b918b0aa65ca39d126d8ce42
Author: luisacicolini <[email protected]>
Date:   Tue Feb 4 12:25:02 2025 +0000

    chore: useless newline

commit a2695ab452057661bcdbc0fd6ab4f64cdd43e5ed
Author: luisacicolini <[email protected]>
Date:   Tue Feb 4 12:08:59 2025 +0000

    chore: first cleaning pass